Skip to content

fixes #1734 (renaming derivable_oo_continuous_bnd)#1747

Merged
affeldt-aist merged 1 commit intomath-comp:masterfrom
affeldt-aist:fix_1734
Nov 6, 2025
Merged

fixes #1734 (renaming derivable_oo_continuous_bnd)#1747
affeldt-aist merged 1 commit intomath-comp:masterfrom
affeldt-aist:fix_1734

Conversation

@affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Nov 4, 2025

Motivation for this change

fixes #1734

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@affeldt-aist affeldt-aist requested a review from t6s November 4, 2025 10:14
@affeldt-aist affeldt-aist added this to the 1.14.0 milestone Nov 4, 2025
@affeldt-aist affeldt-aist added the renaming/refactoring 🔧 This is about a renaming or refactoring in the library label Nov 4, 2025
@affeldt-aist affeldt-aist requested a review from zstone1 November 4, 2025 10:35
t6s
t6s reviewed Nov 5, 2025
View reviewed changes
Copy link
Member

@t6s t6s left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The changes look consistent.

The capital letters L and R in those identifiers look a bit intimidating.
If this is the result of some previous discussion, I will approve this PR, not resuming the issue.
If not, what about naming them like derivable_oo_continuous_cc, derivable_oy_continous_cy, etc.?

@t6s
Copy link
Member

t6s commented Nov 6, 2025

The changes look consistent.

The capital letters L and R in those identifiers look a bit intimidating. If this is the result of some previous discussion, I will approve this PR, not resuming the issue. If not, what about naming them like derivable_oo_continuous_cc, derivable_oy_continous_cy, etc.?

@affeldt-aist suggested using these names (the ones I listed) for lemmas rather than predicates, and I approved that.

@affeldt-aist affeldt-aist merged commit dbc9e07 into math-comp:master Nov 6, 2025
46 checks passed
yosakaon pushed a commit to yosakaon/analysis that referenced this pull request Dec 4, 2025
@affeldt-aist @yosakaon
fixes math-comp#1734 (math-comp#1747)
2c9bd74
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@zstone1 zstone1 Awaiting requested review from zstone1

1 more reviewer

@t6s t6s t6s left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

renaming/refactoring 🔧 This is about a renaming or refactoring in the library

Projects

None yet

Milestone

1.14.0

Development

Successfully merging this pull request may close these issues.

proposal renaming for derivable_oo_continuous_bnd

2 participants

@affeldt-aist @t6s